Inference at * 1 
Iof proof for Lemma p-mu-exists:



1. P : 
2. n:. ((P(n)))
  x: + Top. p-mu(P;x) 

latex

 by ((ExRepD) 
CollapseTHEN ((((if (((first_nat 2:n)) = 0) then (Repeat (MoveToConcl (-1)
C)) else (RepeatFor (first_nat 2:n) (MoveToConcl (-1))))) 
CollapseTHEN (((CompleteInductionOnNat
C) 
CollapseTHEN (((Auto) 
CollapseTHEN (((Decide i:{0..n}. ((P(i))) 
) 
CollapseTHENA (
CoAuto)))))))))) 

latex

Co1: 

Co1: 2. n : 
Co1: 3. n1:. (n1 < n)  ((P(n1)))  (x: + Top. p-mu(P;x))
Co1: 4. (P(n))
Co1: 5. i:{0..n}. ((P(i)))
Co1:   x: + Top. p-mu(P;x)
Co2: 

Co2: 2. n : 
Co2: 3. n1:. (n1 < n)  ((P(n1)))  (x: + Top. p-mu(P;x))
Co2: 4. (P(n))
Co2: 5. (i:{0..n}. ((P(i))))
Co2:   x: + Top. p-mu(P;x)
Co.

Definitions	x:A. B(x), {i..j}, #$n, b, f(a), S  T, |g|, Void, n - m, n+m, -n, i  j , , A, False, p-mu(P;x), Top, x. t(x), (xL.P(x)), xL. P(x), x f y, A c B, a < b, a <p b, a  b, a ~ b, b | a, P  Q, Dec(P), P  Q, left + right, x.A(x), {x:A| B(x)} , i  j < k, P & Q, x:A  B(x), , , a < b, , Type, A  B, x:A. B(x), x:AB(x), t  T, s = t
Lemmas	ge wf, nat properties, nat ind tp, comp nat ind tp, p-mu wf, nat wf, top wf, decidable ex int seg, decidable assert, assert wf, le wf, int seg wf